Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:	if(true,x,y)	→ x
2:	if(false,x,y)	→ y
3:	if(x,y,y)	→ y
4:	if(if(x,y,z),u,v)	→ if(x,if(y,u,v),if(z,u,v))
5:	if(x,if(x,y,z),z)	→ if(x,y,z)
6:	if(x,y,if(x,y,z))	→ if(x,y,z)

There are 3 dependency pairs:


7:	IF(if(x,y,z),u,v)	→ IF(x,if(y,u,v),if(z,u,v))
8:	IF(if(x,y,z),u,v)	→ IF(y,u,v)
9:	IF(if(x,y,z),u,v)	→ IF(z,u,v)

Consider the SCC {7-9}. By taking the AF π with π(IF) = 1 together with the lexicographic path order with empty precedence, the rules in {1-9} are strictly decreasing. Hence the TRS is terminating.

Tyrolean Termination Tool (0.03 seconds) --- May 4, 2006